
% Eventuell Verifikation nach MC
\begin{frame}
\frametitle{Einleitung}
\begin{itemize}
\item Insbesondere bei sicherheitsrelevanten Anwendungen ist es un\-ab\-ding\-bar, dass das tatsächliche Verhalten einer Anwendung dem erwarteten Verhalten einer Anwendung entspricht.
\item Für die Phasen der (Software-)Entwicklung existieren verschiedene Techniken der Qualitätssicherung, z.B:
\begin{itemize}
\item (Unit-)Tests
\item \emph{Model-Checking}
\item Formale Verifikation
\end{itemize}
\end{itemize}
\end{frame}

\begin{frame}
\frametitle{Model-Checking}
\begin{columns}
\column{.5\textwidth}
\begin{itemize}
\item Beim \emph{Model-Checking} wird für ein gegebenes Modell überprüft, ob eine Spezifikation erfüllt ist.
\item Die Verifikation geschieht in der Regel vollautomatisch mithilfe von Modellprüfern (engl. \emph{model checkers})
\item Das \emph{Model-Checking} basiert auf temporalen Logiken wie z.B. CTL.
\end{itemize}
\column{.5\textwidth}
	\begin{center}	
	\begin{tikzpicture}[auto]
	\node [draw,rounded corners,minimum width=2cm,minimum height=1cm] (a) at (-1.5,0) {Modell};
	\node [draw,rounded corners,minimum height=1cm] (b) at (1.5,0) {Spezifikation};
	\node [draw,rounded corners,minimum height=1cm] (c) at (0,-2) {\emph{Model-Checking}};
	\node [draw,rounded corners,minimum height=1cm,color=red, line width=0.8mm] (d) at (-1.5,-4) {Gegenbeispiel};
	\node [draw,rounded corners,minimum height=1cm,minimum width=2cm,color=darkgreen, line width=0.8mm] (e) at (1.5,-4) {Beweis};

	\draw (a) [->,thick] to node {} (c);
	\draw (b) [->,thick] to node {} (c);
	\draw (c) [->,thick] to node {} (d);
	\draw (c) [->,thick] to node {} (e);
	\draw (d) [->,bend left,dashed,color=red] to node {} (a);
		
	\end{tikzpicture}
	\end{center}
\end{columns}
\end{frame}

\begin{frame}
\frametitle{Model-Checking im V-Modell}
\begin{center}
\includegraphics[scale=0.50]{images/vmodell-eps-converted-to.pdf}
\end{center}
\begin{exampleblock}{Aufgabe: Model-Checking im V-Modell}
In welcher Phase des V-Modells kommt \emph{Model-Checking} zum Einsatz?
\end{exampleblock}
\end{frame}


% Eine Folie / Notiz im Vortrag, fehlt noch:
% Was kann man alles Model-Checken?
% z.B. Simulink-Modelle, aber auch generierten Code
